A:Type, eq:EqDecider(A), f, g:a:A fp Top, x:A, z:Top. f  g(x)?z ~ f(x)?g(x)?z 

latex

Definitions	t  T, x:A. B(x), x  dom(f), b, {T}, P  Q, False, P  Q, A, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, Type, s ~ t, x:AB(x), EqDecider(T), a:A fp B(a), x:A. B(x), Top, True, Prop, left+right, x.A(x), x. t(x), f  g, x:AB(x), P & Q, P  Q, b, , s = t, Unit, Void, f(x)?z
Lemmas	fpf wf, deq wf, fpf-join-ap-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, not functionality wrt iff, fpf-join-dom, fpf-join wf, top wf, assert wf, fpf-dom wf